$\forall$${\it es}$:ES, ${\it ff}$:FIFO, $p$:(E$\rightarrow\mathbb{P}$), $e$:E, ${\it sndr}$, ${\it rcvr}$:${\it ff}$.C.
\\[0ex]($\forall$$e$:E. Dec($p$($e$)))
\\[0ex]$\Rightarrow$ ($\forall$$e$:E. Dec(${\it ff}$.S(${\it rcvr}$,${\it sndr}$,$e$)))
\\[0ex]$\Rightarrow$ ($\forall$$e$:E. Dec(${\it ff}$.R(${\it sndr}$,$e$)))
\\[0ex]$\Rightarrow$ Dec([$e$: ${\it sndr}$ $\leftarrow$$p$$--$ ${\it rcvr}$])